Date: Friday, 17-Jan-97 00:08:35 GMT
Server: NCSA/1.3
MIME-version: 1.0
Content-type: text/html
Last-modified: Tuesday, 23-Apr-96 21:21:35 GMT
Content-length: 1750

<html>
<title>Formal Verification of the K5 Divide Program</title>
<!-- Changed by: Tom Lynch,  5-Apr-1996 -->
<head>
<H1 ALIGN="center">Formal Verification of the K5 Divide Program</H1>
</head>
<body>


<Table border=1>
  <tr>

  <td align="left">
    <P>
     <IMG SRC="../images/grey.gif" width=14 height=14 ALT="o">
     <A HREF="affiliation.ps">author affiliations</A>
     <IMG SRC="../images/disk.gif" ALT="" width=11 height=11>
     <IMG SRC="../images/speed1.gif" ALT="" width=4 height=11>
    </P>
    <P>
     <IMG SRC="../images/grey.gif" width=14 height=14 ALT="o">
     <A HREF="colloquia.html">colloquia anouncement</A>
    </P>
     <P><IMG SRC="../images/grey.gif" width=14 height=14 ALT="o">
     <A HREF="abstract.html">abstract</A>
    </P>

    <P>
     <IMG SRC="../images/grey.gif" width=14 height=14 ALT="o">
     <A HREF="divide_paper.ps">technical report explaining how the proof works</A>
     <IMG SRC="../images/disk.gif" ALT="" width=11 height=11>
     <IMG SRC="../images/speed1.gif" ALT="" width=4 height=11>
    </P>

    <P>
     <IMG SRC="../images/grey.gif" width=14 height=14 ALT="o">
     <A HREF="divide_proof.html">the ACL2 based proof</A>
    </P>
  </td>

  <td align="right">
    <address> <IMG SRC="../images/mailto.gif" ALT="" width=14 height=10>
              <A HREF="mailto:moore@cli.com">moore@cli.com</A>
    </address>
    <address> <IMG SRC="../images/mailto.gif" ALT="" width=14 height=10>
              <A HREF="mailto:Tom.Lynch@amd.com">Tom.Lynch@amd.com</A>
    </address>
    <address> <IMG SRC="../images/mailto.gif" ALT="" width=14 height=10>
           <A HREF="mailto:Matt_Kaufmann@email.mot.com">Matt_Kaufmann@email.mot.com</A>
    </address>

  </td>
  </tr>
</table>
</body>
</html>



